#pragma once

#include <iostream>
#include <cctype>

#include "problem_factory.h"
#include "istrategy.h"
#include "problem_solver.h"
#include "file_data.h"

namespace sat
{

	class sat_solver_strategy : public solver::istrategy
	{
		static const int val_normal = 1;
		static const int val_not = 0;

	public:

		virtual int int_to_name(int k)
		{
			return k < -1 ? -k : k;
		}

		virtual solver::variable_value int_to_spin(int v)
		{
			if (v < 0) {
				return val_not;
			}
			return val_normal;
		}

	};

	class cnf_sat_solver
	{
		int current_line_number = 0;

		typedef const char *(cnf_sat_solver::*line_function)(const char *);
		line_function current_line_function;
		std::vector<int> current_clause;
		solver::problem_factory factory;
		int trace_variable = -1;

		const char *read_white(const char *cnf_file_contents)
		{
			while (*cnf_file_contents == ' ' || *cnf_file_contents == '\t')
				cnf_file_contents++;
			return cnf_file_contents;
		}

		const char *read_eol(const char *cnf_file_contents)
		{
			current_line_number++;
			while (*cnf_file_contents == '\r' || *cnf_file_contents == '\n')
				cnf_file_contents++;
			return cnf_file_contents;
		}

		bool is_eol(const char *cnf_file_contents)
		{
			return (*cnf_file_contents == '\r' || *cnf_file_contents == '\n' || *cnf_file_contents == 0);
		}

		const char *read_line(const char *cnf_file_contents)
		{
			cnf_file_contents = read_eol(cnf_file_contents);
			cnf_file_contents = read_white(cnf_file_contents);
			switch (*cnf_file_contents)
			{
			case 'P':
			case 'p':
				current_line_function = &cnf_sat_solver::read_problem_line;
				break;
			case 'C':
			case 'c':
				current_line_function = &cnf_sat_solver::read_comment_line;
				break;
			case 't': // our cnf supports a t variableid number that traces from that variable
				current_line_function = &cnf_sat_solver::read_trace_line;
				break;
			case '-':
			case '0':
			case '1':
			case '2':
			case '3':
			case '4':
			case '5':
			case '6':
			case '7':
			case '8':
			case '9':
				current_line_function = &cnf_sat_solver::read_clause_line;
				break;
			default:
				current_line_function = &cnf_sat_solver::read_other_line;
				std::cout << "line " << current_line_number << ": invalid line" << std::endl;
			}
			return cnf_file_contents;
		}

		const char *read_int(const char *cnf_file_contents, int *intr)
		{
			char buffer[256];
			int max_chars = sizeof(buffer) - 2;
			int count = 0;

			cnf_file_contents = read_white(cnf_file_contents);
			if (*cnf_file_contents == '-')
			{
				buffer[count++] = '-';
				cnf_file_contents++;
				cnf_file_contents = read_white(cnf_file_contents);
			}

			if (!std::isdigit(*cnf_file_contents))
			{
				std::cout << "line " << current_line_number << ": invalid integer" << std::endl;
				cnf_file_contents = read_other_line(cnf_file_contents);
				return cnf_file_contents;
			}

			while (std::isdigit(*cnf_file_contents) && count < max_chars)
			{
				buffer[count++] = *cnf_file_contents;
				cnf_file_contents++;
			}

			buffer[count++] = 0;
			*intr = strtol(buffer, nullptr, 10);

			return cnf_file_contents;
		}

		const char *read_problem_line(const char *cnf_file_contents)
		{
			while (!is_eol(cnf_file_contents))
				cnf_file_contents++;

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

		const char *read_comment_line(const char *cnf_file_contents)
		{
			while (!is_eol(cnf_file_contents))
				cnf_file_contents++;

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

		const char *read_clause_line(const char *cnf_file_contents)
		{

			while (!is_eol(cnf_file_contents))
			{
				int variable = 0;
				cnf_file_contents = read_int(cnf_file_contents, &variable);

				if (variable != 0)
				{
					current_clause.push_back(variable);
				}
				else
				{
					sat_solver_strategy strategy;
					factory.add_clause(0, current_clause.size(), &current_clause[0], &strategy);
					current_clause.clear();
				}
			}

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

		const char *read_trace_line(const char *cnf_file_contents)
		{
			cnf_file_contents++;
			if (!is_eol(cnf_file_contents))
			{
				int variable = 0;
				cnf_file_contents = read_int(cnf_file_contents, &variable);

				if (variable != 0)
				{
					trace_variable = variable;
				}
			}

			while (!is_eol(cnf_file_contents))
				cnf_file_contents++;

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

		const char *read_other_line(const char *cnf_file_contents)
		{
			while (!is_eol(cnf_file_contents))
				cnf_file_contents++;

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

	public:

		solver::problem_solver *create_problem(solver::file_data& data, std::function<void(const char *message)> progress_func)
		{
			trace_variable = -1;

			factory.clear();
			factory.progress_func = progress_func;

			if (progress_func)
				progress_func("Loading file");

			const char *cnf_file_contents = data.get_data();

			solver::problem_solver *sat_prob = new solver::problem_solver();

			if (progress_func)
				progress_func("Parsing File");

			current_line_function = &cnf_sat_solver::read_line;

			int line_count = 0;

			while (*cnf_file_contents)
			{
				cnf_file_contents = (this->*current_line_function)(cnf_file_contents);
				if (progress_func)
				{
					char buff[256];
					sprintf(buff, "Parse %d", ++line_count);
					progress_func(buff);
				}
			}

			if (progress_func)
				progress_func("Creating Problem");

			factory.create_problem(*sat_prob, trace_variable, data.get_file_name().c_str());

			sat_prob->trace_enabled = trace_variable > -1;

			return sat_prob;
		}

		bool solve(solver::file_data& data, bool dump)
		{
			auto sat_prob = create_problem(data, nullptr);

			sat_solver_strategy strategy;

			sat_prob->solve(strategy);

			delete sat_prob;

			return true;
		}
	};
}

